ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), k:Knd, l:IdLnk. msg-item(ds; da; k; l)  Type 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, IdLnk, void, rcv(l,tg), Kind-deq, x.A(x), fpf-cap(f; eq; x; z), type List, ma-valtype(da; k), x:AB(x), decl-state(ds), , x:A  B(x), msg-item(ds; da; k; l)
Lemmas	nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Kind-deq wf, rcv wf, IdLnk wf, Knd wf, fpf wf, Id wf